Termination Proof Script

• Consider the SCC {17,24}. There are no usable rules. By taking the AF π with π(F) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 17 is weakly decreasing and rule 24 is strictly decreasing. There is one new SCC.
  • Consider the SCC {17}. By taking the AF π with π(F) = 1 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.


• Consider the SCC {18,25}. There are no usable rules. By taking the AF π with π(G) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 18 is weakly decreasing and rule 25 is strictly decreasing. There is one new SCC.
  • Consider the SCC {18}. By taking the AF π with π(G) = 1 together with the lexicographic path order with empty precedence, rule 18 is strictly decreasing.


• Consider the SCC {14,16}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(f) = 1 together with the lexicographic path order with empty precedence, rule 14 is weakly decreasing and rule 16 is strictly decreasing. There is one new SCC.
  • Consider the SCC {14}. By taking the AF π with π(ACTIVE) = 1 and π(f) = [1] together with the lexicographic path order with empty precedence, rule 14 is strictly decreasing.


• Consider the SCC {20,21,23}. There are no usable rules. By taking the AF π with π(g) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 23 is weakly decreasing and the rules in {20,21} are strictly decreasing. There is one new SCC.
  • Consider the SCC {23}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 23 is strictly decreasing.


• Consider the SCC {26,28}. The usable rules are {1-9}. By taking the AF π with π(f) = π(g) = π(TOP) = 1 and π(active) = π(mark) = π(ok) = π(proper) = [ ] together with the lexicographic path order with precedence ok ≻ active ≻ mark ≻ proper, the rules in {2-9} are weakly decreasing and the rules in {1,26,28} are strictly decreasing.